es:ES, L:(E List), e:E, i:Id.
loc-on-path(es;i;[e / L])  ((loc(e) = i)  loc-on-path(es;i;L)) 

latex

Definitions	ES, loc-on-path(es;i;L), type List, E, Id, s = t, {T}, P  Q, left + right, x:AB(x), x:A. B(x), t  T, strong-subtype(A;B), P  Q, loc(e), P  Q, x:A  B(x), P & Q, P  Q, [], [car / cdr], as @ bs, s ~ t
Lemmas	member singleton, event system wf, es-E wf, iff functionality wrt iff, loc-on-path-append, iff wf, rev implies wf, Id wf, loc-on-path wf